/*
 * Purity.java
 *
 * Copyright 2007 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.examples;

/**
 * @author csallner@gatech.edu (Christoph Csallner)
 */
public class Purity {

  int field = 5;
  
  int getField() {
    return field;
  }
  
  
  /**
   * Subsequent field read access yields same result:
   * ESC/Java proves field!=null for division.
   * No ESC/Java warning.
   */
  public int fieldAccessPure() {
    if (field==0)
      return 0;
    
    return 10/field;
  }
  
  
  /**
   * Subsequent getField method call may not yield same result.
   * ESC/Java cannot prove (without specification for getField()) that
   * subsequent getField() calls produce the same result.
   * ESC/Java produces false bug warning.
   */
  public int getFieldImPure() {
    if (getField()==0)
      return 0;
    
    return 10/getField();
  }  
}
